*****************************************************************
YQJ from equivalential calculus

(define mp
  {--> prop}
  -> [all x [all y [[[p [e x y]] & [p x]] => [p y]]]])       

(define yqj
  {--> prop}
   -> [all x [all y [all z [p [e [e x y] [e [e z x] [e y z]]]]]]])
   
(define ec   
  {--> prop}
   -> [[[p [e x x]] & [p [e [e x y] [e y x]]]] 
                               & [p [e [e x y] [e [e y z] [e x z]]]]]) 
                               
(kb-> [(mp) (yqj)])

(<-kb (ec))
run time: 1.265625 secs
1745565 inferences, equality = false
depth = 13, complexity = -1, timeout = 60 secs
true
*****************************************************************  
Step 1

? (((p (e x x)) & (p (e (e x y) (e y x)))) & (p (e (e x y) (e (e y z) (e x z)))))


> revsk
=============================
Step 2

? (((p (e x x)) & (p (e (e x y) (e y x)))) & (p (e (e x y) (e (e y z) (e x z)))))


> &r
|=============================
|Step 3
|
|? ((p (e x x)) & (p (e (e x y) (e y x))))
|
|
|> &r
||=============================
||Step 4
||
||? (p (e x x))
||
||
||> hypdisj
||=============================
||Step 5
||
||? (p (e x x))
||
||
||> ((p X) <-- (p (e Y X)) (p Y))
|||=============================
|||Step 6
|||
|||? (p (e Var317 (e x x)))
|||
|||
|||> ((p X) <-- (p (e Y X)) (p Y))
||||=============================
||||Step 7
||||
||||? (p (e Var320 (e Var317 (e x x))))
||||
||||
||||> ((p X) <-- (p (e Y X)) (p Y))
|||||=============================
|||||Step 8
|||||
|||||? (p (e Var323 (e Var320 (e Var317 (e x x)))))
|||||
|||||
|||||> ((p X) <-- (p (e Y X)) (p Y))
||||||=============================
||||||Step 9
||||||
||||||? (p (e (e Var332 Var320) (e (e (e Var317 (e x x)) Var332) (e Var320 (e Var317 (e x x))))))
||||||
||||||
||||||> ((p (e (e X Y) (e (e Z X) (e Y Z)))) <--)
|||||=============================
|||||Step 10
|||||
|||||? (p (e (e Var338 Var339) (e (e Var340 Var338) (e Var339 Var340))))
|||||
|||||
|||||> ((p (e (e X Y) (e (e Z X) (e Y Z)))) <--)
||||=============================
||||Step 11
||||
||||? (p (e (e Var317 (e x x)) (e Var338 Var339)))
||||
||||
||||> ((p X) <-- (p (e Y X)) (p Y))
|||||=============================
|||||Step 12
|||||
|||||? (p (e (e (e x x) Var338) (e (e Var339 (e x x)) (e Var338 Var339))))
|||||
|||||
|||||> ((p (e (e X Y) (e (e Z X) (e Y Z)))) <--)
||||=============================
||||Step 13
||||
||||? (p (e (e x x) (e (e Var353 x) (e x Var353))))
||||
||||
||||> ((p (e (e X Y) (e (e Z X) (e Y Z)))) <--)
|||=============================
|||Step 14
|||
|||? (p (e (e (e (e (e Var353 x) (e x Var353)) Var359) (e (e Var353 x) (e x Var353))) (e (e Var359 (e (e (e Var353 x) (e x Var353)) Var359)) (e (e (e Var353 x) (e x Var353)) Var359))))
|||
|||
|||> ((p (e (e X Y) (e (e Z X) (e Y Z)))) <--)
||=============================
||Step 15
||
||? (p (e (e (e x x) (e x x)) (e (e (e x x) (e x x)) (e (e x x) (e x x)))))
||
||
||> ((p (e (e X Y) (e (e Z X) (e Y Z)))) <--)
|=============================
|Step 16
|
|? (p (e (e x y) (e y x)))
|
|
|> hypdisj
|=============================
|Step 17
|
|? (p (e (e x y) (e y x)))
|
|
|> ((p X) <-- (p (e Y X)) (p Y))
||=============================
||Step 18
||
||? (p (e (e y y) (e (e x y) (e y x))))
||
||
||> ((p (e (e X Y) (e (e Z X) (e Y Z)))) <--)
|=============================
|Step 19
|
|? (p (e y y))
|
|
|> ((p X) <-- (p (e Y X)) (p Y))
||=============================
||Step 20
||
||? (p (e Var377 (e y y)))
||
||
||> ((p X) <-- (p (e Y X)) (p Y))
|||=============================
|||Step 21
|||
|||? (p (e Var380 (e Var377 (e y y))))
|||
|||
|||> ((p X) <-- (p (e Y X)) (p Y))
||||=============================
||||Step 22
||||
||||? (p (e Var383 (e Var380 (e Var377 (e y y)))))
||||
||||
||||> ((p X) <-- (p (e Y X)) (p Y))
|||||=============================
|||||Step 23
|||||
|||||? (p (e (e Var392 Var380) (e (e (e Var377 (e y y)) Var392) (e Var380 (e Var377 (e y y))))))
|||||
|||||
|||||> ((p (e (e X Y) (e (e Z X) (e Y Z)))) <--)
||||=============================
||||Step 24
||||
||||? (p (e (e Var398 Var399) (e (e Var400 Var398) (e Var399 Var400))))
||||
||||
||||> ((p (e (e X Y) (e (e Z X) (e Y Z)))) <--)
|||=============================
|||Step 25
|||
|||? (p (e (e Var377 (e y y)) (e Var398 Var399)))
|||
|||
|||> ((p X) <-- (p (e Y X)) (p Y))
||||=============================
||||Step 26
||||
||||? (p (e (e (e y y) Var398) (e (e Var399 (e y y)) (e Var398 Var399))))
||||
||||
||||> ((p (e (e X Y) (e (e Z X) (e Y Z)))) <--)
|||=============================
|||Step 27
|||
|||? (p (e (e y y) (e (e Var413 y) (e y Var413))))
|||
|||
|||> ((p (e (e X Y) (e (e Z X) (e Y Z)))) <--)
||=============================
||Step 28
||
||? (p (e (e (e (e (e Var413 y) (e y Var413)) Var419) (e (e Var413 y) (e y Var413))) (e (e Var419 (e (e (e Var413 y) (e y Var413)) Var419)) (e (e (e Var413 y) (e y Var413)) Var419))))
||
||
||> ((p (e (e X Y) (e (e Z X) (e Y Z)))) <--)
|=============================
|Step 29
|
|? (p (e (e (e y y) (e y y)) (e (e (e y y) (e y y)) (e (e y y) (e y y)))))
|
|
|> ((p (e (e X Y) (e (e Z X) (e Y Z)))) <--)
=============================
Step 30

? (p (e (e x y) (e (e y z) (e x z))))


> hypdisj
=============================
Step 31

? (p (e (e x y) (e (e y z) (e x z))))


> ((p X) <-- (p (e Y X)) (p Y))
|=============================
|Step 32
|
|? (p (e Var430 (e (e x y) (e (e y z) (e x z)))))
|
|
|> ((p X) <-- (p (e Y X)) (p Y))
||=============================
||Step 33
||
||? (p (e (e Var439 (e x y)) (e (e (e (e y z) (e x z)) Var439) (e (e x y) (e (e y z) (e x z))))))
||
||
||> ((p (e (e X Y) (e (e Z X) (e Y Z)))) <--)
|=============================
|Step 34
|
|? (p (e Var439 (e x y)))
|
|
|> ((p X) <-- (p (e Y X)) (p Y))
||=============================
||Step 35
||
||? (p (e Var442 (e Var439 (e x y))))
||
||
||> ((p X) <-- (p (e Y X)) (p Y))
|||=============================
|||Step 36
|||
|||? (p (e (e Var451 Var439) (e (e (e x y) Var451) (e Var439 (e x y)))))
|||
|||
|||> ((p (e (e X Y) (e (e Z X) (e Y Z)))) <--)
||=============================
||Step 37
||
||? (p (e (e Var457 Var458) (e (e Var459 Var457) (e Var458 Var459))))
||
||
||> ((p (e (e X Y) (e (e Z X) (e Y Z)))) <--)
|=============================
|Step 38
|
|? (p (e (e x y) (e (e Var465 x) (e y Var465))))
|
|
|> ((p (e (e X Y) (e (e Z X) (e Y Z)))) <--)
=============================
Step 39

? (p (e (e (e y z) (e x z)) (e (e Var459 (e Var465 x)) (e (e y Var465) Var459))))


> ((p X) <-- (p (e Y X)) (p Y))
|=============================
|Step 40
|
|? (p (e Var468 (e (e (e y z) (e x z)) (e (e Var459 (e Var465 x)) (e (e y Var465) Var459)))))
|
|
|> ((p X) <-- (p (e Y X)) (p Y))
||=============================
||Step 41
||
||? (p (e Var471 (e Var468 (e (e (e y z) (e x z)) (e (e Var459 (e Var465 x)) (e (e y Var465) Var459))))))
||
||
||> ((p X) <-- (p (e Y X)) (p Y))
|||=============================
|||Step 42
|||
|||? (p (e (e Var480 Var468) (e (e (e (e (e y z) (e x z)) (e (e Var459 (e Var465 x)) (e (e y Var465) Var459))) Var480) (e Var468 (e (e (e y z) (e x z)) (e (e Var459 (e Var465 x)) (e (e y Var465) Var459)))))))
|||
|||
|||> ((p (e (e X Y) (e (e Z X) (e Y Z)))) <--)
||=============================
||Step 43
||
||? (p (e (e Var486 Var487) (e (e Var488 Var486) (e Var487 Var488))))
||
||
||> ((p (e (e X Y) (e (e Z X) (e Y Z)))) <--)
|=============================
|Step 44
|
|? (p (e (e (e (e y z) (e x z)) (e (e Var459 (e Var465 x)) (e (e y Var465) Var459))) (e Var486 Var487)))
|
|
|> ((p X) <-- (p (e Y X)) (p Y))
||=============================
||Step 45
||
||? (p (e Var491 (e (e (e (e y z) (e x z)) (e (e Var459 (e Var465 x)) (e (e y Var465) Var459))) (e Var486 Var487))))
||
||
||> ((p X) <-- (p (e Y X)) (p Y))
|||=============================
|||Step 46
|||
|||? (p (e Var494 (e Var491 (e (e (e (e y z) (e x z)) (e (e Var459 (e Var465 x)) (e (e y Var465) Var459))) (e Var486 Var487)))))
|||
|||
|||> ((p X) <-- (p (e Y X)) (p Y))
||||=============================
||||Step 47
||||
||||? (p (e (e Var503 Var491) (e (e (e (e (e (e y z) (e x z)) (e (e Var459 (e Var465 x)) (e (e y Var465) Var459))) (e Var486 Var487)) Var503) (e Var491 (e (e (e (e y z) (e x z)) (e (e Var459 (e Var465 x)) (e (e y Var465) Var459))) (e Var486 Var487))))))
||||
||||
||||> ((p (e (e X Y) (e (e Z X) (e Y Z)))) <--)
|||=============================
|||Step 48
|||
|||? (p (e (e Var509 Var510) (e (e Var511 Var509) (e Var510 Var511))))
|||
|||
|||> ((p (e (e X Y) (e (e Z X) (e Y Z)))) <--)
||=============================
||Step 49
||
||? (p (e (e (e (e (e y z) (e x z)) (e (e Var459 (e Var465 x)) (e (e y Var465) Var459))) (e Var486 Var487)) (e Var509 Var510)))
||
||
||> ((p X) <-- (p (e Y X)) (p Y))
|||=============================
|||Step 50
|||
|||? (p (e (e (e Var486 Var487) Var509) (e (e (e (e (e y z) (e x z)) (e (e Var459 (e Var465 x)) (e (e y Var465) Var459))) (e Var486 Var487)) (e Var509 (e (e (e y z) (e x z)) (e (e Var459 (e Var465 x)) (e (e y Var465) Var459)))))))
|||
|||
|||> ((p (e (e X Y) (e (e Z X) (e Y Z)))) <--)
||=============================
||Step 51
||
||? (p (e (e Var522 Var523) (e (e Var524 Var522) (e Var523 Var524))))
||
||
||> ((p (e (e X Y) (e (e Z X) (e Y Z)))) <--)
|=============================
|Step 52
|
|? (p (e (e (e (e (e x z) (e z x)) (e (e y z) (e x z))) (e (e x z) (e z x))) (e (e (e (e y z) (e x z)) (e (e (e x z) (e z x)) (e (e y z) (e x z)))) (e (e (e x z) (e z x)) (e (e y z) (e x z))))))
|
|
|> ((p (e (e X Y) (e (e Z X) (e Y Z)))) <--)
=============================
Step 53

? (p (e (e Var488 z) (e z Var488)))


> ((p X) <-- (p (e Y X)) (p Y))
|=============================
|Step 54
|
|? (p (e Var531 (e (e Var488 z) (e z Var488))))
|
|
|> ((p X) <-- (p (e Y X)) (p Y))
||=============================
||Step 55
||
||? (p (e Var534 (e Var531 (e (e Var488 z) (e z Var488)))))
||
||
||> ((p X) <-- (p (e Y X)) (p Y))
|||=============================
|||Step 56
|||
|||? (p (e (e Var543 Var531) (e (e (e (e Var488 z) (e z Var488)) Var543) (e Var531 (e (e Var488 z) (e z Var488))))))
|||
|||
|||> ((p (e (e X Y) (e (e Z X) (e Y Z)))) <--)
||=============================
||Step 57
||
||? (p (e Var543 Var531))
||
||
||> ((p X) <-- (p (e Y X)) (p Y))
|||=============================
|||Step 58
|||
|||? (p (e (e Var552 Var553) (e (e Var554 Var552) (e Var553 Var554))))
|||
|||
|||> ((p (e (e X Y) (e (e Z X) (e Y Z)))) <--)
||=============================
||Step 59
||
||? (p (e (e Var560 Var561) (e (e Var562 Var560) (e Var561 Var562))))
||
||
||> ((p (e (e X Y) (e (e Z X) (e Y Z)))) <--)
|=============================
|Step 60
|
|? (p (e (e (e Var488 z) (e z Var488)) (e (e Var561 (e Var488 z)) (e (e z Var488) Var561))))
|
|
|> ((p (e (e X Y) (e (e Z X) (e Y Z)))) <--)
=============================
Step 61

? (p (e (e (e Var562 (e z Var488)) (e Var561 Var562)) (e Var561 (e Var488 z))))


> ((p X) <-- (p (e Y X)) (p Y))
|=============================
|Step 62
|
|? (p (e Var569 (e (e (e Var562 (e z Var488)) (e Var561 Var562)) (e Var561 (e Var488 z)))))
|
|
|> ((p X) <-- (p (e Y X)) (p Y))
||=============================
||Step 63
||
||? (p (e (e Var578 (e (e Var562 (e z Var488)) (e Var561 Var562))) (e (e (e Var561 (e Var488 z)) Var578) (e (e (e Var562 (e z Var488)) (e Var561 Var562)) (e Var561 (e Var488 z))))))
||
||
||> ((p (e (e X Y) (e (e Z X) (e Y Z)))) <--)
|=============================
|Step 64
|
|? (p (e Var578 (e (e Var562 (e z Var488)) (e Var561 Var562))))
|
|
|> ((p X) <-- (p (e Y X)) (p Y))
||=============================
||Step 65
||
||? (p (e (e Var587 (e Var562 (e z Var488))) (e (e (e Var561 Var562) Var587) (e (e Var562 (e z Var488)) (e Var561 Var562)))))
||
||
||> ((p (e (e X Y) (e (e Z X) (e Y Z)))) <--)
|=============================
|Step 66
|
|? (p (e (e Var593 z) (e (e Var488 Var593) (e z Var488))))
|
|
|> ((p (e (e X Y) (e (e Z X) (e Y Z)))) <--)
=============================
Step 67

? (p (e (e Var561 (e Var488 z)) (e (e Var561 (e Var488 Var593)) (e Var593 z))))


> ((p X) <-- (p (e Y X)) (p Y))
|=============================
|Step 68
|
|? (p (e (e (e Var488 z) (e (e Var593 z) (e Var488 Var593))) (e (e (e Var593 z) (e Var488 z)) (e (e (e Var593 z) (e Var488 Var593)) (e Var593 z)))))
|
|
|> ((p (e (e X Y) (e (e Z X) (e Y Z)))) <--)
=============================
Step 69

? (p (e (e z z) (e (e Var593 z) (e z Var593))))


> ((p (e (e X Y) (e (e Z X) (e Y Z)))) <--)
